\begin{tabbing}
interleaving\_occurence($T$;$L_{1}$;$L_{2}$;$L$;$f_{1}$;$f_{2}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\parallel$$L$$\parallel$ $=$ $\parallel$$L_{1}$$\parallel$+$\parallel$$L_{2}$$\parallel$ $\in$ $\mathbb{N}$\+
\\[0ex]\& increasing($f_{1}$;$\parallel$$L_{1}$$\parallel$) \& ($\forall$$j$:\{0..$\parallel$$L_{1}$$\parallel^{-}$\}. $L_{1}$[$j$] $=$ $L$[$f_{1}$($j$)] $\in$ $T$)
\\[0ex]\& increasing($f_{2}$;$\parallel$$L_{2}$$\parallel$) \& ($\forall$$j$:\{0..$\parallel$$L_{2}$$\parallel^{-}$\}. $L_{2}$[$j$] $=$ $L$[$f_{2}$($j$)] $\in$ $T$)
\\[0ex]\& ($\forall$$j_{1}$:\{0..$\parallel$$L_{1}$$\parallel^{-}$\}, $j_{2}$:\{0..$\parallel$$L_{2}$$\parallel^{-}$\}. $\neg$$f_{1}$($j_{1}$) $=$ $f_{2}$($j_{2}$) $\in$ $\mathbb{Z}$)
\-
\end{tabbing}